Nuprl Lemma : increasing_wf
11,40
postcript
pdf
k
:
,
f
:(int_seg(0;
k
)
). increasing(
f
;
k
)
prop{i:l}
latex
Definitions
False
,
P
Q
,
A
,
P
Q
,
lelt(
i
;
j
;
k
)
,
A
B
,
increasing(
f
;
k
)
,
prop{i:l}
,
t
T
,
int_seg(
i
;
j
)
,
x
:
A
.
B
(
x
)
,
Lemmas
nat
wf
,
le
wf
,
int
seg
wf
origin
k:
, f:(int_seg(0; k)
). increasing(f; k) 
prop{i:l} k:, f:(int_seg(0; k)). increasing(f; k) prop{i:l} 
Q
A
Q
B Tx:A. B(x)